#pragma once

#include "formula/aalta_formula.h"
#include "ltlf2dfa/mona_ext.h"
#include "ltlf2dfa/syft_ext.h"
#include <cstring>
#include <unordered_set>

class Synthesis
{
  public:
    Synthesis(aalta::aalta_formula *src_formula, std::unordered_set<std::string> &env_var, std::string partfile, bool verbose);
    bool is_realizable();

  private:
    aalta::aalta_formula *src_formula;
    std::unordered_set<std::string> env_var;
    std::string partfile;
    bool verbose;

    // following vars used when exporting DFA
    int var_num;
    std::vector<std::string> var_names;
    std::vector<char> orders;
    std::vector<unsigned int> var_index;
    std::vector<int> indicies;

    void printDotAndDfaFile_forDebug(DFA *a, std::string file_basename)
    {
#ifdef DEBUG
        printDotAndDfaFile(a, file_basename, var_num, var_index, var_names, orders);
#endif
    }

    std::vector<aalta::aalta_formula *> and_sub_afs_vec;

    bool preCheck_subAfs();
    bool compositional_synthesis();
    void init_forDFA();
    bool check_DFA_realizability(DFA *a)
    {
        return syft_check_synthesis(SynType::SYS_FIRST, a, partfile, var_num, var_names, orders);
    }
};
